package controller.preprocessor;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.concurrent.Semaphore;

import model.cnf.FileCNF;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;

/**
 * <p>
 * This Class provide a model for you to add and implement your own preprocessor. It take care of
 * the maximum of operation so that you only need the give the minimum amount of information and add
 * as quickly as possible your preprocessor.
 * </p>
 * <p>
 * So to add your preprocessor you only need to implement the hasTimeout method, return false if
 * your preprocessor has no timeout, getCommandLine that return the command line that should be run
 * and also checkParameter that check if everything is fine with the parameter (I recommend to
 * create a new Parameter Class). It also provide you a way to to some additional work after the
 * execution by implementing the returnXXXX method that are call after the execution return the XXXX
 * status. Be aware of the returnProblemCNF method.
 * </p>
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public abstract class PreProcessorModel extends PreProcessor {

	/** The default value that is return */
	public static final int	DEFAULT_RETURN_VALUE	= 0;
	/** The default value that is associate to a UNSATISFIABLE result */
	public static final int	RETURN_UNSATISFIABLE	= 20;
	/** The default value that is associate to a SATISFIABLE result */
	public static final int	RETURN_SATISFIABLE		= 10;

	protected int			returnDefault			= DEFAULT_RETURN_VALUE;
	protected int			returnUnSat				= RETURN_UNSATISFIABLE;
	protected int			returnSat				= RETURN_SATISFIABLE;
	protected String		description;

	/**
	 * Create a preprocessor model.
	 * 
	 * @param description
	 *            Description of the solver
	 * @param defaultValue
	 *            value that is return by default
	 * @param sat
	 *            value that is return by the solver when the result is SATISFIABLE
	 * @param unsat
	 *            value that is return by the solver when the result is UNSATISFIABLE
	 */
	public PreProcessorModel(String description, int defaultValue, int unsat, int sat) {
		returnDefault = defaultValue;
		returnUnSat = unsat;
		returnSat = sat;
		this.description = description;
	}

	@Override
	public abstract String[] getCommandLine(String cnfFile);

	@Override
	public abstract boolean hasTimeout();

	@Override
	public PreProcessorResult runPreProcessor(String[] cmd, String fileOutput, Semaphore manager) {
		PreProcessorResult res = new PreProcessorResult();

		BufferedReader input = null;
		BufferedReader inerr = null;
		try
		{// lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			try
			{
				process = Runtime.getRuntime().exec(cmd);
			} catch (IOException e)
			{
				throw e;
			}
			finally
			{// libere les sem
				sem.release();
				if (manager != null)
					manager.release();
			}

			String line;
			input = new BufferedReader(new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader(new InputStreamReader(process.getErrorStream()));

			while ((line = input.readLine()) != null)
				// System.out.println(line);
				res.addStdin(line + "\n");
			while ((line = inerr.readLine()) != null)
				// System.out.println(line);
				res.addStderr(line + "\n");
		} catch (IOException e)
		{
			// e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
			if (process != null)
				process.destroy();
		}
		finally
		{
			try
			{
				if (input != null)
					input.close();
				if (inerr != null)
					inerr.close();
				if (process != null)
					res.setExitVal(process.waitFor());
			} catch (Exception e)
			{
				// e.printStackTrace();
				res.setStatus(PreProcessorResultStatus.PROBLEM);
			}
			finally
			{
				try
				{
					sem.acquire();
				} catch (InterruptedException e)
				{
					// TODO Auto-generated catch block
					e.printStackTrace();
					return null;
				}

				setRunning(false);
			}
		}
		// terminer
		res.setEnd(System.currentTimeMillis());

		// System.out.println("val de retour"+res.getExitVal());

		// s'occupe du status
		if (hasBeenStop())
		{// cas stop
			res.setStatus(PreProcessorResultStatus.STOP);
			returnHasBeenStop(res);
		}
		else
			if (hasBeenTimeout())
			{// cas timeout
				res.setStatus(PreProcessorResultStatus.TIMEOUT_REACHED);
				returnHasBeenTimeout(res);
			}
			else
				if (res.getStatus() != PreProcessorResultStatus.PROBLEM)
					if (res.getExitVal() == returnUnSat)
					{// UNSAT
						res.setStatus(PreProcessorResultStatus.UNSATISFIABLE);
						returnUnSat(res);
					}
					else
						if (res.getExitVal() == returnSat)
						{// SAT
							res.setStatus(PreProcessorResultStatus.SATISFIABLE);
							returnUnSat(res);
						}
						else
							if (res.getExitVal() == returnDefault)
							{ // DEFAULT
								res.setStatus(PreProcessorResultStatus.OK);
								returnDefault(res);
							}
							else
							{// PROBLEM
								res.setStatus(PreProcessorResultStatus.PROBLEM);
								returnProblem(res);
							}

		// dernier details
		res.setDescription(description);
		res.setExportPath(fileOutput);
		try
		{
			if (res.getStatus() == PreProcessorResultStatus.OK)
				res.setCnf(new FileCNF(fileOutput));
			// res.setStat(new Stat(res.getCnf()));
		} catch (Exception e)
		{
			// e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
			returnProblemCNF(res);
		}

		// libere le sem
		sem.release();

		return res;
	}

	/**
	 * Is call when the preprocessor was executed without problem.
	 * 
	 * @param res
	 *            the actual result of the preprocessing
	 */
	protected abstract void returnDefault(PreProcessorResult res);

	/**
	 * Is call when the result after the execution of the preprocessor is UNSAT.
	 * 
	 * @param res
	 *            the actual result of the preprocessing
	 */
	protected abstract void returnUnSat(PreProcessorResult res);

	/**
	 * Is call when there was a problem.
	 * 
	 * @param res
	 *            the actual result of the preprocessing
	 */
	protected abstract void returnProblem(PreProcessorResult res);

	/**
	 * Is call when there was a problem creating the result CNF : this operation is done at last,
	 * after everything else, it means also that one of the other returnXXX method has been call
	 * before.
	 * 
	 * @param res
	 *            the actual result of the preprocessing
	 */
	protected abstract void returnProblemCNF(PreProcessorResult res);

	/**
	 * Is call after the execution of the preprocessor has been stop by the timeout.
	 * 
	 * @param res
	 *            the actual result of the solving
	 */
	protected abstract void returnHasBeenTimeout(PreProcessorResult res);

	/**
	 * Is call after the execution of the preprocessor has been stop.
	 * 
	 * @param res
	 *            the actual result of the preprocessing
	 */
	protected abstract void returnHasBeenStop(PreProcessorResult res);

}
